1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
/*!
Contexts for substituting terms
*/

use super::*;

mod slice;
mod vec;
mod down;

pub use slice::*;
pub use vec::*;
pub use down::*;

/// A context for substituting terms
pub trait SubstCtx {
    /// This type's underlying context
    type Ctx: TyCtxMut;

    #[inline]
    /// Cache a substitution result. May cause erroneous behaviour if the result passed is invalid!
    ///
    /// May return an error on invalid input, though this is *not* guaranteed.
    fn cache(&mut self, _term: &TermId, _subst: Option<&TermId>) -> Result<(), Error> {
        Ok(())
    }

    /// Attempt to substitute an entire term. Return `None` if substitution should proceed recursively instead.
    #[inline]
    fn try_subst(&mut self, _term: &Term) -> Option<Result<Option<TermId>, Error>> {
        None
    }

    /// Substutite a variable, with an optional *un-substituted* annotation, adding the annotation as a constraint.
    ///
    /// Returns an error if the annotation gives a type error. Implementations may return an error when provided a null annotation,
    /// or may perform a substitution with no constraint.
    fn subst_constrain(
        &mut self,
        ix: u32,
        annot: Option<&TermId>,
    ) -> Result<Option<TermId>, Error> {
        if let Some(annot) = annot {
            if let Some(false) = self.ctx().constrain(ix, annot)? {
                return Err(Error::TypeMismatch);
            }
        }
        self.subst_var(ix, annot)
    }

    /// Substutite a variable, with an optional *un-substituted* annotation. Does *not* add the annotation as a constraint.
    ///
    /// Returns an error if the annotation gives a type error. Implementations may return an error when provided a null annotation,
    /// or may perform a substitution with no constraint.
    fn subst_var(&mut self, ix: u32, annot: Option<&TermId>) -> Result<Option<TermId>, Error>;

    /// Push a parameter onto this context with an optional annotation, returning the annotation substitution, if any
    fn push_param(&mut self, param_ty: Option<&TermId>) -> Result<Option<TermId>, Error>;

    /// Check whether this context can potentially make any changes to a term with the given filter
    fn intersects(&self, filter: VarFilter, code: Code, form: Form) -> bool;

    /// Get the underlying context
    fn ctx(&mut self) -> &mut Self::Ctx;

    /// Get the underlying consing context
    #[inline]
    fn cons_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::ConsCtx {
        self.ctx().cons_ctx()
    }

    /// Get the underlying equality context
    #[inline]
    fn eq_ctx(&mut self) -> &mut <Self::Ctx as TyCtxMut>::TermEqCtx {
        self.ctx().eq_ctx()
    }

    /// Push a parameter onto the underlying context with an optional annotation
    #[inline]
    fn push_param_ctx(&mut self, param_ty: Option<&TermId>) -> Result<(), Error> {
        self.ctx().push_param(param_ty)
    }

    /// Pop a parameter from this context
    fn pop_param(&mut self) -> Result<(), Error>;

    /// Whether no variables are substituted by this context
    fn is_var_null(&self) -> bool;
}

/// A context for evaluating terms
pub trait EvalCtx: SubstCtx {
    /// Push a substitution onto this context
    fn push_subst(&mut self, subst: TermId) -> Result<(), Error>;
    /// Pop a substitution from this context
    fn pop_subst(&mut self) -> Result<(), Error>;
}